from automata.fa.nfa import NFA
from hazard_value.helpers import *
import igraph
import numpy
import json

# load a nfa from a given json file

def load_nfa (filename):

# open the file and load its content

	f = open(filename)
	nfa_dict = json.loads(f.read())
	f.close()

	if not isinstance(nfa_dict, dict): 
		raise ValueError("File "+filename+" does not contain a valid json dictionary.")

# init the different fields of the nfa

	states = {0}
	input_symbols = {"."}
	transitions = {0:dict()}
	final_states = set()

# init the set of input symbols and the regex

	regex = None
	symbols = dict()
	symbols["."] = {"."}

	for key in nfa_dict:
		if key=="regex": regex = nfa_dict[key]
		else:
			if not isinstance(nfa_dict[key], list): 
				raise ValueError("Non regex key "+key+" must refer to a list.")
			else:
				symbols[key] = set()
				for edge in nfa_dict[key]:
					if not isinstance(edge, list): raise ValueError("Item "+str(edge)+" is not a list.")
					elif not len(edge)==2: raise ValueError(str(edge)+" must contain 2 values.")
					edge = tuple(edge)
					symbols[key].add(edge)
					input_symbols.add(edge)

# build the transition function by parsing the regex

	if regex is None: raise ValueError ("No regex is specified in your language.")
	current_state = 0
	old_state = 0
	root = 0

	for c in regex:
		if c==" " or c=="\t": continue # skip white spaces
		elif c == "*": # star a regex
			trans = transitions[old_state]
			for edge in trans:
				if current_state in trans[edge]: 
					trans[edge] = (trans[edge]-{current_state})|{old_state}

			states.remove(current_state)
			transitions.pop(current_state)
			current_state = old_state
		elif c == "+": # star a regex
			trans = transitions[old_state]
			edges = list(filter(lambda e: current_state in trans[e], trans))
			for symbol in edges:
				if symbol in transitions[current_state]: 
					transitions[current_state][symbol].add(current_state)
				else:
					transitions[current_state][symbol] = {current_state}

		elif c=="|": # create an alternative branch
			final_states.add(current_state)
			current_state = root
			previous_state = root

		elif c in symbols: # if a new symbol is found create a transition
			old_state = current_state
			current_state = len(states)
			states.add(current_state)
			transitions[current_state] = dict()
			for symbol in symbols[c]:
				if symbol in transitions[old_state]: 
					transitions[old_state][symbol].add(current_state)
				else:
					transitions[old_state][symbol] = {current_state}
		else: # otherwise raise a value error
			raise ValueError("Unknown symbol: "+c)

# finally returns the built nfa

	final_states.add(current_state)
	return NFA(states=states, input_symbols=input_symbols, transitions=transitions, initial_state=0, final_states=final_states)


# check that t is reachable from s in a graph g under a failure scenario f and path constraints nfa

def check_nfa_reach (g, s, t, f, nfa, Q=None):

# init the variables

	pending = {s}
	tau = dict()
	tau[s] = {nfa.initial_state} if Q is None else Q

# while it remains some nodes to explore and that the target has not been reached yet

	while pending:
		u = pending.pop()
		label1 = g.vs[u]["label"]

# explore all running outgoing edges of u

		E = set(g.incident(u, mode="out"))
		E = E - f

		for e in E:
			v = g.es[e].target

# compute the set of successor states after having read e

			label2 = g.vs[v]["label"]
			edge1 = (label1, label2)
			edge2 = (".", label2)
			X = set()

			for q in tau[u]:
				key = None
				if edge1 in nfa.transitions[q]: key = edge1  
				elif edge2 in nfa.transitions[q]: key = edge2
				elif "." in nfa.transitions[q]: key = "."
				if not (key is None):
					Q = nfa.transitions[q][key]
					X |= Q

# if X is not already part of the explored states attached to v add it to tau(v)

			if not v in tau: 
				pending.add(v)
				tau[v] = X
				if v==t and len(nfa.final_states & X)>0: return True
			elif not (X <= tau[v]):
				pending.add(v)
				tau[v] |= X
				if v==t and len(nfa.final_states & X)>0: return True

	return False

# check that t is reachable from s under the failure scenario f and the oracle path constraints

def check_oracle_reach (g, s, t, f, oracle, Qf, Q0):

# init the sets of pending and passed keys

	if s==t and Q0<=Qf: return True
	key = (s, frozenset(Q0))
	pending = {key}
	passed = {key}

# explore the oracle while it remains some key in it

	while pending:
		key = pending.pop()

# if t in reached in an acceptance state returns true; otherwise add all successors to pending

		if key[0]==t and len(Qf & key[1])>0: return True
		elif not key[0] in oracle: continue
		else:
			for q in key[1]:
				if not q in oracle[key[0]]: continue
				keys = oracle[key[0]][q]
				for e in keys:
					if oracle[key[0]][q][e] in passed or e in f: continue
					pending.add(oracle[key[0]][q][e])
					passed.add(oracle[key[0]][q][e])

	return False

# reuse some already known reachability results

def reuse_reachability_result(g, s, t, oracle, edges, Qf, Q0):

# init the stacks of keys and edges

	pending = {(s, Q0)}
	passed = set(pending)

# while it remains some keys to explore add all successor edges and corresponding keys

	while pending:
		u, Q = pending.pop()
		for q in Q:
			for e in oracle[u][q]:
				v, Q0 = oracle[u][q][e]
				if not check_oracle_reach(g, v, t, set(), oracle, Qf, Q0): continue
				edges[q].add(e)
				if not oracle[u][q][e] in passed:
					pending.add(oracle[u][q][e])
					passed.add(oracle[u][q][e])

# compute the product automaton between nfa path constraints and paths from a source s to a target t

def compute_nfa_used_edges (g, s, t, nfa, oracle=dict()):

	# init the variables
	edges = {q:set() for q in nfa.states}
	tau = dict()
	tau[s] = {nfa.initial_state}

	pending = {s}
	new_oracle = {s:{0:dict()}}

	# while all paths have not been explored yet
	while pending:
		u = pending.pop()
		label1 = g.vs[u]["label"]

		# if the key is already known in the oracle reuse the corresponding reachability results
		Q0 = frozenset(oracle[u].keys()) if u in oracle else set()
		Qf = frozenset(oracle[t].keys() & nfa.final_states) if t in oracle else None

		if tau[u]<=Q0 and Qf:
			reuse_reachability_result(g, u, t, oracle, edges, Qf, Q0)
			continue

		# otherwise explore all running outgoing edges of u
		E = set(g.incident(u, mode="out"))

		for e in E:
			v = g.es[e].target
			# compute the set of successor states after having read e
			label2 = g.vs[v]["label"]
			edge1 = (label1, label2)
			edge2 = (".", label2)
			X = set()
			if not v in new_oracle: new_oracle[v] = dict()

			for q in tau[u]:
				key = None
				if edge1 in nfa.transitions[q]: key = edge1  
				elif edge2 in nfa.transitions[q]: key = edge2
				elif "." in nfa.transitions[q]: key = "."
				if not (key is None):
					Q = nfa.transitions[q][key]
					X |= Q
					# update the oracle
					if not q in new_oracle[u]: new_oracle[u][q]=dict()
					new_oracle[u][q][e] = (v, frozenset(Q))

			if v==t and len(X & nfa.final_states)>0 or check_nfa_reach(g, v, t, set(), nfa, X): 
				for q in tau[u]:
					edges[q].add(e)

			# if X is not already part of the explored states attached to v add it to tau(v)
			if not v in tau or not (X <= tau[v]): 
					pending.add(v)
					tau[v] = tau[v]|X if v in tau else X

	# finally update the oracle and return the used edges
	for u in new_oracle:
		if not u in oracle: oracle[u] = new_oracle[u]
		else: 
			for q in new_oracle[u]:
				if q in oracle[u]: oracle[u][q].update(new_oracle[u][q])
				else: oracle[u][q] = new_oracle[u][q]

	return edges


# compute the change points of a graph

def compute_change_points (g, nfa):

# loop over all states of the automaton

	change_points = dict()
	labels = dict()

	for q in nfa.states:
		change_points[q] = dict()
		Q = {q}

# loop over all label key of the current state and add it to labels if it changes something

		for label in nfa.transitions[q]:
			if nfa.transitions[q][label]!=Q:
				if not label in labels: labels[label] = {q:nfa.transitions[q][label]}
				elif not q in labels[label]: labels[label][q] = nfa.transitions[q][label]
				else: labels[label][q] |= Q

# finally match all edges of the graph to their corresponding label and extract the change points

	for e in g.es:
		u_label = g.vs[e.source]["label"]
		v_label = g.vs[e.target]["label"]
		label = (u_label, v_label)
		if not label in labels: continue
		for q in labels[label]: change_points[q][e.target] = labels[label][q]
	return change_points